es:event_system{i:l}, e:es-E(es). es-le(es; es-init(es;e); e)  True 

latex

Definitions	ff, tt, if b then t else f fi , P  Q, P  Q, Y, final-iterate(f; x), x. t(x), P  Q, prop{i:l}, t  T, True, es-init(es;e), P  Q, x:A. B(x), Unit, , P  Q, guard(T), x(s), es-locl(es; e; e'), wellfounded{i:l}(A; x,y.R(x;y)), es-le(es; e; e'),
Lemmas	not functionality wrt iff, eqff to assert, assert of bnot, eqtt to assert, iff transitivity, es-le weakening eq, es-le weakening, es-locl transitivity1, es-pred-locl, es-pred wf, do-apply-pred?, not wf, assert wf, bool wf, es-first wf, bnot wf, event system wf, es-locl wf, can-apply-pred?, es-E wf, true wf, es-init wf, es-le wf, iff wf, es-locl-wellfnd